equiv_rel(b-union(; (:  int_nzero)); r,s.(qeq(r; s) = tt  )) 

latex

Definitions	guard(T), sq_type(T), P  Q, P  Q, prop{i:l}, P  Q, t  T, ff, if b then t else f fi , x:A. B(x), trans(T; x,y.E(x;y)), sym(T; x,y.E(x;y)), refl(T; x,y.E(x;y)), P  Q, tt, qeq(r; s), equiv_rel(T; x,y.E(x;y)), , int_nzero, b-union(A; B)
Lemmas	mul assoc, mul com, mul cancel in eq, btrue wf, qeq wf, bool wf, int nzero wf, b-union wf, assert of eq int, eq int wf, eqtt to assert